0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳12 CpxRNTS
↳13 InliningProof (UPPER BOUND(ID), 232 ms)
↳14 CpxRNTS
↳15 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 209 ms)
↳20 CpxRNTS
↳21 IntTrsBoundProof (UPPER BOUND(ID), 37 ms)
↳22 CpxRNTS
↳23 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 103 ms)
↳26 CpxRNTS
↳27 IntTrsBoundProof (UPPER BOUND(ID), 36 ms)
↳28 CpxRNTS
↳29 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 208 ms)
↳32 CpxRNTS
↳33 IntTrsBoundProof (UPPER BOUND(ID), 63 ms)
↳34 CpxRNTS
↳35 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳36 CpxRNTS
↳37 IntTrsBoundProof (UPPER BOUND(ID), 34 ms)
↳38 CpxRNTS
↳39 IntTrsBoundProof (UPPER BOUND(ID), 57 ms)
↳40 CpxRNTS
↳41 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳42 CpxRNTS
↳43 IntTrsBoundProof (UPPER BOUND(ID), 156 ms)
↳44 CpxRNTS
↳45 IntTrsBoundProof (UPPER BOUND(ID), 14 ms)
↳46 CpxRNTS
↳47 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳48 CpxRNTS
↳49 IntTrsBoundProof (UPPER BOUND(ID), 63 ms)
↳50 CpxRNTS
↳51 IntTrsBoundProof (UPPER BOUND(ID), 67 ms)
↳52 CpxRNTS
↳53 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳54 CpxRNTS
↳55 IntTrsBoundProof (UPPER BOUND(ID), 123 ms)
↳56 CpxRNTS
↳57 IntTrsBoundProof (UPPER BOUND(ID), 53 ms)
↳58 CpxRNTS
↳59 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳60 CpxRNTS
↳61 IntTrsBoundProof (UPPER BOUND(ID), 254 ms)
↳62 CpxRNTS
↳63 IntTrsBoundProof (UPPER BOUND(ID), 63 ms)
↳64 CpxRNTS
↳65 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳66 CpxRNTS
↳67 IntTrsBoundProof (UPPER BOUND(ID), 4051 ms)
↳68 CpxRNTS
↳69 IntTrsBoundProof (UPPER BOUND(ID), 338 ms)
↳70 CpxRNTS
↳71 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳72 CpxRNTS
↳73 IntTrsBoundProof (UPPER BOUND(ID), 115 ms)
↳74 CpxRNTS
↳75 IntTrsBoundProof (UPPER BOUND(ID), 44 ms)
↳76 CpxRNTS
↳77 FinalProof (⇔, 0 ms)
↳78 BOUNDS(1, n^1)
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
2ndspos(0, Z) → rnil
plus(0, Y) → Y
activate(X) → X
times(0, Y) → 0
cons(X1, X2) → n__cons(X1, X2)
activate(n__s(X)) → s(activate(X))
square(X) → times(X, X)
activate(n__from(X)) → from(activate(X))
from(X) → cons(X, n__from(n__s(X)))
pi(X) → 2ndspos(X, from(0))
from(X) → n__from(X)
s(X) → n__s(X)
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
2ndsneg(0, Z) → rnil
2ndspos(0, Z) → rnil [1]
plus(0, Y) → Y [1]
activate(X) → X [1]
times(0, Y) → 0 [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__s(X)) → s(activate(X)) [1]
square(X) → times(X, X) [1]
activate(n__from(X)) → from(activate(X)) [1]
from(X) → cons(X, n__from(n__s(X))) [1]
pi(X) → 2ndspos(X, from(0)) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [1]
2ndsneg(0, Z) → rnil [1]
2ndspos(0, Z) → rnil [1]
plus(0, Y) → Y [1]
activate(X) → X [1]
times(0, Y) → 0 [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__s(X)) → s(activate(X)) [1]
square(X) → times(X, X) [1]
activate(n__from(X)) → from(activate(X)) [1]
from(X) → cons(X, n__from(n__s(X))) [1]
pi(X) → 2ndspos(X, from(0)) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(n__cons(X1, X2)) → cons(activate(X1), X2) [1]
2ndsneg(0, Z) → rnil [1]
2ndspos :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from → rnil 0 :: 0:n__cons:n__s:n__from rnil :: rnil plus :: 0:n__cons:n__s:n__from → plus → plus activate :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from times :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from cons :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from n__cons :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from n__s :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from s :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from square :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from n__from :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from from :: 0:n__cons:n__s:n__from → 0:n__cons:n__s:n__from pi :: 0:n__cons:n__s:n__from → rnil 2ndsneg :: 0:n__cons:n__s:n__from → a → rnil |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
2ndspos
plus
times
square
pi
2ndsneg
activate
from
s
cons
const, const1
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
rnil => 0
const => 0
const1 => 0
2ndsneg(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ s(s(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ s(from(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ from(s(activate(X3))) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 2 }→ from(from(activate(X4))) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
from(z) -{ 1 }→ cons(X, 1 + (1 + X)) :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
pi(z) -{ 2 }→ 2ndspos(X, cons(0, 1 + (1 + 0))) :|: X >= 0, z = X
pi(z) -{ 2 }→ 2ndspos(X, 1 + 0) :|: X >= 0, z = X
plus(z, z') -{ 1 }→ Y :|: z' = Y, Y >= 0, z = 0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
square(z) -{ 1 }→ times(X, X) :|: X >= 0, z = X
times(z, z') -{ 1 }→ 0 :|: z' = Y, Y >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
times(z, z') -{ 1 }→ 0 :|: z' = Y, Y >= 0, z = 0
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
from(z) -{ 1 }→ cons(X, 1 + (1 + X)) :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
2ndsneg(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ s(s(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ s(from(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(X3))) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 2 }→ from(from(activate(X4))) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
from(z) -{ 2 }→ 1 + X1 + X2 :|: X >= 0, z = X, X1 >= 0, X2 >= 0, X = X1, 1 + (1 + X) = X2
pi(z) -{ 3 }→ 2ndspos(X, 1 + X1 + X2) :|: X >= 0, z = X, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: X >= 0, z = X, Z >= 0, 1 + 0 = Z, X = 0
plus(z, z') -{ 1 }→ Y :|: z' = Y, Y >= 0, z = 0
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
square(z) -{ 2 }→ 0 :|: X >= 0, z = X, X = Y, Y >= 0, X = 0
times(z, z') -{ 1 }→ 0 :|: z' = Y, Y >= 0, z = 0
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
{ from } { 2ndsneg } { cons } { 2ndspos } { s } { times } { square } { plus } { activate } { pi } |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: ?, size: O(n1) [3 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: ?, size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: ?, size: O(n1) [1 + z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 3 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: ?, size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: ?, size: O(n1) [1 + z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: ?, size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: ?, size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] plus: runtime: ?, size: O(n1) [z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] plus: runtime: O(1) [1], size: O(n1) [z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] plus: runtime: O(1) [1], size: O(n1) [z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] plus: runtime: O(1) [1], size: O(n1) [z'] activate: runtime: ?, size: EXP |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(cons(activate(X1'), X2')) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(cons(activate(X1''), X2'')) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ cons(s(activate(X5)), X2) :|: X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(from(activate(X6)), X2) :|: X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ 2 }→ cons(cons(activate(X11), X21), X2) :|: z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] plus: runtime: O(1) [1], size: O(n1) [z'] activate: runtime: O(n1) [11 + 37·z], size: EXP |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 15 + 37·X5 }→ s11 :|: s9 >= 0, s9 <= inf1, s10 >= 0, s10 <= 1 * s9 + 1, s11 >= 0, s11 <= 1 * s10 + 1 * X2 + 1, X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ -57 + 37·z }→ s14 :|: s12 >= 0, s12 <= inf2, s13 >= 0, s13 <= 2 * s12 + 3, s14 >= 0, s14 <= 2 * s13 + 3, z - 2 >= 0
activate(z) -{ 16 + 37·X1'' }→ s17 :|: s15 >= 0, s15 <= inf3, s16 >= 0, s16 <= 1 * s15 + 1 * X2'' + 1, s17 >= 0, s17 <= 2 * s16 + 3, X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 15 + 37·X11 }→ s2 :|: s'' >= 0, s'' <= inf, s1 >= 0, s1 <= 1 * s'' + 1 * X21 + 1, s2 >= 0, s2 <= 1 * s1 + 1 * X2 + 1, z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 16 + 37·X6 }→ s20 :|: s18 >= 0, s18 <= inf4, s19 >= 0, s19 <= 2 * s18 + 3, s20 >= 0, s20 <= 1 * s19 + 1 * X2 + 1, X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ -58 + 37·z }→ s23 :|: s21 >= 0, s21 <= inf5, s22 >= 0, s22 <= 2 * s21 + 3, s23 >= 0, s23 <= 1 * s22 + 1, z - 2 >= 0
activate(z) -{ -58 + 37·z }→ s26 :|: s24 >= 0, s24 <= inf6, s25 >= 0, s25 <= 1 * s24 + 1, s26 >= 0, s26 <= 2 * s25 + 3, z - 2 >= 0
activate(z) -{ -59 + 37·z }→ s5 :|: s3 >= 0, s3 <= inf', s4 >= 0, s4 <= 1 * s3 + 1, s5 >= 0, s5 <= 1 * s4 + 1, z - 2 >= 0
activate(z) -{ 15 + 37·X1' }→ s8 :|: s6 >= 0, s6 <= inf'', s7 >= 0, s7 <= 1 * s6 + 1 * X2' + 1, s8 >= 0, s8 <= 1 * s7 + 1, z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] plus: runtime: O(1) [1], size: O(n1) [z'] activate: runtime: O(n1) [11 + 37·z], size: EXP |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 15 + 37·X5 }→ s11 :|: s9 >= 0, s9 <= inf1, s10 >= 0, s10 <= 1 * s9 + 1, s11 >= 0, s11 <= 1 * s10 + 1 * X2 + 1, X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ -57 + 37·z }→ s14 :|: s12 >= 0, s12 <= inf2, s13 >= 0, s13 <= 2 * s12 + 3, s14 >= 0, s14 <= 2 * s13 + 3, z - 2 >= 0
activate(z) -{ 16 + 37·X1'' }→ s17 :|: s15 >= 0, s15 <= inf3, s16 >= 0, s16 <= 1 * s15 + 1 * X2'' + 1, s17 >= 0, s17 <= 2 * s16 + 3, X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 15 + 37·X11 }→ s2 :|: s'' >= 0, s'' <= inf, s1 >= 0, s1 <= 1 * s'' + 1 * X21 + 1, s2 >= 0, s2 <= 1 * s1 + 1 * X2 + 1, z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 16 + 37·X6 }→ s20 :|: s18 >= 0, s18 <= inf4, s19 >= 0, s19 <= 2 * s18 + 3, s20 >= 0, s20 <= 1 * s19 + 1 * X2 + 1, X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ -58 + 37·z }→ s23 :|: s21 >= 0, s21 <= inf5, s22 >= 0, s22 <= 2 * s21 + 3, s23 >= 0, s23 <= 1 * s22 + 1, z - 2 >= 0
activate(z) -{ -58 + 37·z }→ s26 :|: s24 >= 0, s24 <= inf6, s25 >= 0, s25 <= 1 * s24 + 1, s26 >= 0, s26 <= 2 * s25 + 3, z - 2 >= 0
activate(z) -{ -59 + 37·z }→ s5 :|: s3 >= 0, s3 <= inf', s4 >= 0, s4 <= 1 * s3 + 1, s5 >= 0, s5 <= 1 * s4 + 1, z - 2 >= 0
activate(z) -{ 15 + 37·X1' }→ s8 :|: s6 >= 0, s6 <= inf'', s7 >= 0, s7 <= 1 * s6 + 1 * X2' + 1, s8 >= 0, s8 <= 1 * s7 + 1, z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] plus: runtime: O(1) [1], size: O(n1) [z'] activate: runtime: O(n1) [11 + 37·z], size: EXP pi: runtime: ?, size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 15 + 37·X5 }→ s11 :|: s9 >= 0, s9 <= inf1, s10 >= 0, s10 <= 1 * s9 + 1, s11 >= 0, s11 <= 1 * s10 + 1 * X2 + 1, X5 >= 0, z = 1 + (1 + X5) + X2, X2 >= 0
activate(z) -{ -57 + 37·z }→ s14 :|: s12 >= 0, s12 <= inf2, s13 >= 0, s13 <= 2 * s12 + 3, s14 >= 0, s14 <= 2 * s13 + 3, z - 2 >= 0
activate(z) -{ 16 + 37·X1'' }→ s17 :|: s15 >= 0, s15 <= inf3, s16 >= 0, s16 <= 1 * s15 + 1 * X2'' + 1, s17 >= 0, s17 <= 2 * s16 + 3, X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 15 + 37·X11 }→ s2 :|: s'' >= 0, s'' <= inf, s1 >= 0, s1 <= 1 * s'' + 1 * X21 + 1, s2 >= 0, s2 <= 1 * s1 + 1 * X2 + 1, z = 1 + (1 + X11 + X21) + X2, X11 >= 0, X21 >= 0, X2 >= 0
activate(z) -{ 16 + 37·X6 }→ s20 :|: s18 >= 0, s18 <= inf4, s19 >= 0, s19 <= 2 * s18 + 3, s20 >= 0, s20 <= 1 * s19 + 1 * X2 + 1, X6 >= 0, z = 1 + (1 + X6) + X2, X2 >= 0
activate(z) -{ -58 + 37·z }→ s23 :|: s21 >= 0, s21 <= inf5, s22 >= 0, s22 <= 2 * s21 + 3, s23 >= 0, s23 <= 1 * s22 + 1, z - 2 >= 0
activate(z) -{ -58 + 37·z }→ s26 :|: s24 >= 0, s24 <= inf6, s25 >= 0, s25 <= 1 * s24 + 1, s26 >= 0, s26 <= 2 * s25 + 3, z - 2 >= 0
activate(z) -{ -59 + 37·z }→ s5 :|: s3 >= 0, s3 <= inf', s4 >= 0, s4 <= 1 * s3 + 1, s5 >= 0, s5 <= 1 * s4 + 1, z - 2 >= 0
activate(z) -{ 15 + 37·X1' }→ s8 :|: s6 >= 0, s6 <= inf'', s7 >= 0, s7 <= 1 * s6 + 1 * X2' + 1, s8 >= 0, s8 <= 1 * s7 + 1, z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
square(z) -{ 2 }→ 0 :|: z >= 0, z = 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] s: runtime: O(1) [1], size: O(n1) [1 + z] times: runtime: O(1) [1], size: O(1) [0] square: runtime: O(1) [2], size: O(1) [0] plus: runtime: O(1) [1], size: O(n1) [z'] activate: runtime: O(n1) [11 + 37·z], size: EXP pi: runtime: O(1) [4], size: O(1) [0] |